Add eggcc container benchmark#8
Closed
saulshanabrook wants to merge 13 commits into
Closed
Conversation
…gcc-container-benchmark
6f0d26e3 Merge pull request #927 from oflatt/oflatt-container-proofs 85ba2626 small feedback fixes 4141a970 Merge pull request #935 from egraphs-good/nightly 5009aaee simplify map.rs e45cd547 address feedback from Saul 3960015c Merge pull request #885 from saulshanabrook/codex/split-scheduler-stale-match-cleanup bd1697a3 Tighten the Containers section of proof_encoding.md (#10) 5fca83b7 Add container support to the term/proof encoding 7f111370 nightly: prefer the rustup cargo shim over the system cargo (#942) 15888b87 nightly: install deps into a venv to satisfy PEP 668 (#939) f295052e scheduler: skip subsumed fresh matches d1418d20 Merge remote-tracking branch 'upstream/main' into codex/split-scheduler-stale-match-cleanup f99482a2 Merge pull request #936 from oflatt-claude/nightly-eval-live fe240e6b Render nightly benchmark report with eval-live 5bb42afc nightly 6c6f01d5 scheduler: simplify changelog entry c1420100 scheduler: reduce held validation churn ce4ef0b5 scheduler: validate only held matches f0d4822b scheduler: keep stale validation focused 1dedb505 scheduler: condense changelog entry 939339b1 scheduler: simplify stale match validation ed6aa6e9 scheduler: preserve existing match handling 8602f56e scheduler: split action-key dedup cleanup 89779541 scheduler: validate only held matches e24d1468 scheduler: clarify stale match validation eaf4ab4f Merge remote-tracking branch 'upstream/main' into codex/split-scheduler-stale-match-cleanup 0804bee1 scheduler: deduplicate residual match keys 2c55caff Merge remote-tracking branch 'upstream/main' into codex/split-scheduler-stale-match-cleanup 09b8c002 scheduler: document stale match validation 2c749b89 scheduler: clean stale matches git-subtree-dir: egglog git-subtree-split: 6f0d26e37241055a1230bdcdb33f0c5d3f01e935
5d24c481 Refresh eggcc proof baseline onto PR 927 core 19ed8666 Remove redundant eggcc helper fixture fcdaccba Add full eggcc proof fixture 6b37b6b3 Add eggcc proof baseline helpers git-subtree-dir: egglog-experimental git-subtree-split: 5d24c48197f796e130457fa2f0c10a60dfe258c7
…gcc-container-benchmark # Conflicts: # egglog-experimental/Cargo.toml # egglog-experimental/src/keep_best.rs # egglog-experimental/src/lib.rs # egglog-experimental/src/set_cost.rs # egglog-experimental/src/sugar/for.rs # egglog-experimental/src/table_stats.rs
a3ace918 Merge index-rebuild blocks with ping-pong buffers 8ed30f98 Use balanced tournament merge for multi-column index rebuild f895dfdb Rebuild ColumnIndex via per-column radix sort + merge 201579af Fix multi-column column index rebuild ordering REVERT: 6f0d26e3 Merge pull request #927 from oflatt/oflatt-container-proofs REVERT: 85ba2626 small feedback fixes REVERT: 4141a970 Merge pull request #935 from egraphs-good/nightly REVERT: 5009aaee simplify map.rs REVERT: e45cd547 address feedback from Saul REVERT: 3960015c Merge pull request #885 from saulshanabrook/codex/split-scheduler-stale-match-cleanup REVERT: bd1697a3 Tighten the Containers section of proof_encoding.md (#10) REVERT: 5fca83b7 Add container support to the term/proof encoding REVERT: 7e926c6e Merge pull request #940 from saulshanabrook/codex/proof-checker-fast-path REVERT: 77d90469 Drop proof checker target early exit REVERT: 9b98ba8d Merge pull request #941 from saulshanabrook/codex/root-proof-extractor REVERT: be2b4b3b Address root proof extractor review feedback REVERT: 02002320 Speed up direct rule proof checks REVERT: 7f111370 nightly: prefer the rustup cargo shim over the system cargo (#942) REVERT: 48715264 Add root-directed proof extraction REVERT: 15888b87 nightly: install deps into a venv to satisfy PEP 668 (#939) REVERT: 64b45484 Merge pull request #930 from egraphs-good/codex/proof-rhs-lookups REVERT: bb20f2c7 Move proof primitive tests out of lib REVERT: f295052e scheduler: skip subsumed fresh matches REVERT: d1418d20 Merge remote-tracking branch 'upstream/main' into codex/split-scheduler-stale-match-cleanup REVERT: 0f506f26 Reject naive eq-sort primitive proof facts REVERT: 42a4fb6a Merge pull request #928 from saulshanabrook/codex/proof-selector-merge-main REVERT: f99482a2 Merge pull request #936 from oflatt-claude/nightly-eval-live REVERT: fe240e6b Render nightly benchmark report with eval-live REVERT: e22580de Merge pull request #929 from egraphs-good/codex/proof-mode-main-fixes REVERT: 5bb42afc nightly REVERT: e4a65359 Name-indexed read/write API on Read/Write traits + EGraph::update (#901) REVERT: 5c124ad9 Handle eq-container fact proof lookups REVERT: 3db22bfb Avoid cloning type info for proof macros REVERT: 0d92ecc7 Support eq-sort primitive fact proofs REVERT: 96b54d02 Handle proof-mode primitive and macro regressions REVERT: 0a868b67 Update proof encoding snapshot REVERT: 1f4f128e Avoid redundant proof merge rows REVERT: 7d102dbd Merge pull request #912 from oflatt/unsafe-seminaive REVERT: 31084c50 review: condense changelog and fix stale Full-context comment (CodeRabbit) REVERT: 97d4c776 review: clarify naming/logic around read contexts (Saul) REVERT: 1475db24 typecheck: gate action-lookup check on effective context, not eval_mode REVERT: 2315ccfc proofs: preserve user :naive through encoding; test against :unsafe-seminaive REVERT: 447eda6a Merge remote-tracking branch 'origin/main' into unsafe-seminaive REVERT: 5e655cae Merge pull request #922 from saulshanabrook/codex/proof-simplifications REVERT: a9eb0d21 Merge pull request #913 from saulshanabrook/saul-proofs REVERT: 6c6f01d5 scheduler: simplify changelog entry REVERT: c1420100 scheduler: reduce held validation churn REVERT: ce4ef0b5 scheduler: validate only held matches REVERT: f0d4822b scheduler: keep stale validation focused REVERT: 1dedb505 scheduler: condense changelog entry REVERT: 939339b1 scheduler: simplify stale match validation REVERT: ed6aa6e9 scheduler: preserve existing match handling REVERT: 8602f56e scheduler: split action-key dedup cleanup REVERT: 89779541 scheduler: validate only held matches REVERT: e24d1468 scheduler: clarify stale match validation REVERT: eaf4ab4f Merge remote-tracking branch 'upstream/main' into codex/split-scheduler-stale-match-cleanup REVERT: 5294cdc6 Merge pull request #881 from saulshanabrook/codex/split-primitive-body-runtime-apis REVERT: 494a2046 :unsafe-seminaive/:naive: collapse to one RuleEvalMode field, error on conflict REVERT: 61b6fa99 improve performance REVERT: 8ceaa013 Simplify generated proof symmetry chains REVERT: 586dbc4b Bump Codecov action for key migration REVERT: 427e6f25 Add baseline proof simplification snapshots REVERT: cb111894 Add term encoding subsume rebuild snapshot REVERT: a2da717f Merge pull request #919 from saulshanabrook/codex/git-size-budget REVERT: 2ba87f46 Avoid duplicating Git size limit defaults REVERT: 07d10ba6 Derive Git size help text from constants REVERT: 3bbc5cf9 Keep Git size limits in script REVERT: 7e66919d Document Git size budget check REVERT: 6e9463bf Add Git size budget check script REVERT: c740e68a Add Git size budget check REVERT: f7161140 Update proof encoding snapshot REVERT: 9ea71cbf Fix math normal overlap REVERT: 9bc1ed9f allow math demo in proof benchmark manually REVERT: 6f03cf80 remove unused var REVERT: ec3fadcd run math and math in proof mode in CI REVERT: 06588cd8 Fix proofs for subsumed union find updates REVERT: 4dbc3a04 Add another rebuild test case REVERT: 879e4cd3 Update DEBUG logging to include every interation of rules and move query plans to TRACE REVERT: df5170a7 Fixes subsumed bugs that were preventing math.egg to run REVERT: 7ac5a350 Rename BackendRule.seminaive -> context_seminaive (Copilot review) REVERT: 9b2d6645 Drop lookups_to_action: query-only callers don't build proofs REVERT: 3590f847 Fix CI: collapse clippy nested-if; add new tests to proof_unsupported snapshot REVERT: 234657f2 test: read-primitive (FullPrim) in an :unsafe-seminaive RHS REVERT: 26b499fc proofs: fetch eq-sort var term_proofs via action lookups, tag :unsafe-seminaive REVERT: 1c6e0911 Add `:unsafe-seminaive` rule option for arbitrary RHS reads REVERT: f0da95b0 Merge pull request #908 from SAY-5/fix-run-undefined-ruleset REVERT: 2a3db9cd Merge pull request #884 from saulshanabrook/codex/split-scheduler-id-validation REVERT: d1b597f6 Merge pull request #900 from egraphs-good/yihozhang-constant-fold-bound-vars REVERT: d57d7604 Return NoSuchRuleset instead of panicking when running an undefined ruleset REVERT: 7cf54265 Fix formatting and clippy nits REVERT: 1a66ccf6 Address review: saturating_mul, doc ColUniqueness, relax lifetime REVERT: 854d194e Merge pull request #876 from egraphs-good/copilot/fix-repl-panic-on-include-failure REVERT: af9f0567 factorized bindings for FusedIntersectMat REVERT: 3ad2c0ef add size estimation to TD. eggcc-extraction 100% slower REVERT: e3f5fc3a Add a simple cardinality estimator REVERT: 84f07105 Refine missing-include test path generation REVERT: 2daa4a72 Handle missing include files without panicking REVERT: a5029f00 Initial plan REVERT: bde27c2e Merge pull request #907 from gleachkr/main REVERT: a80b2351 Return errors for direct unstable-fn preparation REVERT: 6ca134be Merge remote-tracking branch 'upstream/main' into codex/split-primitive-body-runtime-apis REVERT: f854bde2 Support globals in direct expression evaluation REVERT: ddf2656e Use crate hash map for extension state REVERT: 5f0642ae Merge branch 'main' into codex/split-scheduler-id-validation REVERT: e183d4a0 Expose proof reconstruction API REVERT: 42bc6c43 Cover missing extension state lookup REVERT: 399c7058 Add typed egraph extension state REVERT: 0804bee1 scheduler: deduplicate residual match keys REVERT: 2c55caff Merge remote-tracking branch 'upstream/main' into codex/split-scheduler-stale-match-cleanup REVERT: 09b8c002 scheduler: document stale match validation REVERT: 142e07a5 Revert "Leave global handling to explicit evaluators" REVERT: 081498aa Leave global handling to explicit evaluators REVERT: a0ea0add Document resolved eval capability invariant REVERT: efee2299 Reject globals in explicit expression typechecking REVERT: cf4fe23e Fix primitive body eval nits REVERT: 1671a2ed Narrow primitive body eval support REVERT: 4c430f6b Prepare primitive bodies through core actions REVERT: 28d270c7 Address primitive body API review REVERT: 9b7ee1df Add primitive body typecheck helpers REVERT: 2c749b89 scheduler: clean stale matches git-subtree-dir: egglog git-subtree-split: a3ace9187202ef2af11aed244e0515b01b663a84
…gcc-container-benchmark
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: defaults Review profile: CHILL Plan: Pro Run ID: 📒 Files selected for processing (9)
🚧 Files skipped from review as they are similar to previous changes (8)
📝 WalkthroughWalkthroughThis PR adds container-sort support to egglog’s term/proof encoding, including rebuild primitives, proof normalization, and side-condition checking. It also adds Either/Maybe container sorts and merge primitives in egglog-experimental, updates benchmark validation, and adds a nightly benchmark harness. ChangesContainer proof/term encoding in egglog core
egglog-experimental container primitives
Benchmarking infra
Estimated code review effort: 5 (Critical) | ~150 minutes Sequence Diagram(s)sequenceDiagram
participant RebuildRule as Rebuild rule
participant ContainerRebuild as ContainerRebuild primitive
participant ContainerRebuildProof as ContainerRebuildProof primitive
participant CSortProof as CSortProof table
participant ProofStore as Proof checker
RebuildRule->>ContainerRebuild: rebuild container elements via UF leaders
RebuildRule->>ContainerRebuildProof: request rebuild proof for changed elements
ContainerRebuildProof->>CSortProof: read reflexive base proof
ContainerRebuildProof->>ContainerRebuildProof: fold Congr chain over changed children
ContainerRebuildProof->>ContainerRebuildProof: apply ContainerNormalize
ContainerRebuildProof->>CSortProof: anchor new reflexive proof
ProofStore->>ProofStore: check_side_condition re-evaluates container fact
Possibly related PRs
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
Merging this PR will not alter performance
Performance Changes
Comparing 
|
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 2
🧹 Nitpick comments (5)
egglog/scripts/nightly_bench.py (1)
303-355: 🩺 Stability & Availability | 🔵 Trivial | ⚡ Quick winWrap per-benchmark loop body in try/except for nightly resilience.
An unexpected exception from
probe(),hyperfine(), orjson.load()(e.g.,OSError,json.JSONDecodeError) would abort the entire sweep without generating a report. For a nightly harness, one bad benchmark file should not prevent the report from being produced.♻️ Suggested resilience wrapper
for path in benchmarks: name = path.relative_to(TEST_DIR).as_posix() + try: req = requires_proofs(path) # Qualification probes: the single-thread standard run and the proof run. std_probe = None if req else probe(path, 1, False) proof_probe = None if proof_excluded(path) else probe(path, 1, True) proof_supported = proof_probe is not None and proof_probe[0] std_qualifies = std_probe is not None and std_probe[0] and std_probe[1] >= MIN_BENCH_SECONDS proof_qualifies = proof_supported and proof_probe[1] >= MIN_BENCH_SECONDS if not (std_qualifies or proof_qualifies): reason = "errored" if (req and not proof_supported) else "too-fast" skipped.append({"name": name, "reason": reason}) continue cells: dict[str, dict] = {} for key, _label, threads, proof in CONFIGS: if proof: if not proof_supported: cells[key] = {"status": "na"} # proofs unsupported / excluded else: cells[key] = measure_cell(path, threads, True, proof_probe) else: if req: cells[key] = {"status": "na"} # needs proofs; no plain run else: pr = std_probe if threads == 1 else None cells[key] = measure_cell(path, threads, False, pr) # Enforce the threshold on measured data: the cold qualification probe # can overshoot 50ms for a program whose warmed runs are all faster. measured = [c["mean"] for c in cells.values() if "mean" in c] if not measured or max(measured) < MIN_BENCH_SECONDS: skipped.append({"name": name, "reason": "too-fast"}) continue rows.append({"name": name, "cells": cells}) def fmt(key: str) -> str: c = cells[key] return f"{c['mean']:>10.3f}" if "mean" in c else f"{c.get('status', '—'):>10}" log(f" {name:<40} " + " ".join(fmt(k) for k, *_ in CONFIGS)) + except Exception as exc: + log(f" {name:<40} ERROR: {exc}") + skipped.append({"name": name, "reason": "error"}) + continue🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@egglog/scripts/nightly_bench.py` around lines 303 - 355, The per-benchmark processing loop in nightly_bench.py should be made resilient so one failing benchmark does not abort the full report. Wrap the body of the benchmark iteration around the calls to probe(), measure_cell(), hyperfine(), and any JSON loading path in a try/except that catches unexpected exceptions like OSError and json.JSONDecodeError, then record the current benchmark in skipped with an appropriate error reason and continue. Keep the existing row/skip bookkeeping in the loop around benchmark names, and use the existing probe, measure_cell, and skipped/rows flow to preserve output for all remaining benchmarks.egglog/scripts/requirements.txt (1)
1-1: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick winPin
eval-liveto a commit SHA for reproducible nightly runs. The current git dependency tracks the default branch, so upstream changes can break the harness unexpectedly.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@egglog/scripts/requirements.txt` at line 1, The eval-live dependency is currently floating on the default branch, which makes nightly runs non-reproducible; update the requirement in requirements.txt to pin eval-live to a specific commit SHA instead of an unpinned git reference. Keep the existing git-based dependency form, but replace the branch-tracking reference with a commit-specific one so future upstream changes do not alter harness behavior unexpectedly.egglog-experimental/src/maybe.rs (1)
184-264: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick winDuplicated tolerance-merge logic between live primitive and TermDag validator.
The float-tolerance comparison (
old_f == new_f || (old_f == 0.0 && new_f == -0.0) || ... || (old_f - new_f).abs() <= tolerance) is implemented twice — once in thePurePrim-style closure body (Lines 194-198) and again invalidate_maybe_f64_merge_with_tol(Lines 257-260). If one copy is ever tweaked (e.g. tolerance semantics change) without updating the other, generated proofs could validate incorrectly against runtime behavior. Consider extracting the pure numeric comparison into a shared helper function reused by both.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@egglog-experimental/src/maybe.rs` around lines 184 - 264, The float-tolerance merge condition is duplicated between the `maybe-f64-merge-with-tol` primitive closure and `validate_maybe_f64_merge_with_tol`, so update both paths to use one shared helper for the numeric comparison. Extract the `old_f/new_f/tolerance` merge check into a reusable function and call it from both `add_primitive_with_validator!` and the validator, keeping `maybe_sorts`/`maybe_f64` flow unchanged.egglog-experimental/src/container_primitives.rs (1)
193-245: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick winDuplicated min/max comparison logic between
bound_merge(runtime) andvalidate_maybe_either_i64_bool_merge(validator).Both functions independently encode identical
keep_oldboolean logic forMin/Maxoveri64/bool. Consider factoring the comparison predicates (keep_oldfor int/bool givenBoundMergeKind) into small shared helpers to avoid divergence between the live evaluator and the proof-term validator.Also applies to: 304-331
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@egglog-experimental/src/container_primitives.rs` around lines 193 - 245, The `bound_merge` runtime path and `validate_maybe_either_i64_bool_merge` validator duplicate the same `Min`/`Max` keep_old logic for `i64` and `bool`, so refactor that predicate into shared helper(s) and have both functions call them. Use the existing `BoundMergeKind`, `bound_merge`, and `validate_maybe_either_i64_bool_merge` symbols to centralize the comparison behavior and keep the runtime and validator in sync.egglog/tests/files.rs (1)
430-446: 🎯 Functional Correctness | 🔵 Trivial | ⚡ Quick winManual proof-disable list can be silently bypassed for curated integration files.
proof_testingtrials are generated whensupports_proofs || run.is_curated_proof_integration(), butsupports_proofsis the only branch that checksmanual_proof_disable_reason. If a file is ever added to bothPROOF_INTEGRATION_FILESandMANUAL_PROOF_DISABLED_FILES(no overlap today), the disable would be silently ignored for theproof_testingtrial. Worth guarding now to avoid a future footgun.♻️ Proposed guard
- if !should_fail && (supports_proofs || run.is_curated_proof_integration()) { + if !should_fail + && manual_proof_disable_reason(&run.path).is_none() + && (supports_proofs || run.is_curated_proof_integration()) + {🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@egglog/tests/files.rs` around lines 430 - 446, The proof trial generation in files.rs can bypass the manual proof-disable guard for curated integration files because the check for manual_proof_disable_reason only runs under supports_proofs, while is_curated_proof_integration() still enables proof_testing trials. Update the trial-building logic around push_trial in the proof-testing branch so manual_proof_disable_reason is consulted before adding any proof_testing or desugar proof trials, regardless of whether the run came from supports_proofs or is_curated_proof_integration(). Use the existing Run fields and the proof integration gating in this loop to keep disabled files from ever producing proof trials.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@egglog-experimental/tests/eggcc_2mm_proof.rs`:
- Around line 30-66: The required-string assertions in
eggcc_2mm_full_export_uses_container_helpers currently scan the raw program
text, so comment-only mentions can satisfy them. Reuse the non_comment_program
filtering already built in this test and check the required list against that
cleaned text instead of program, especially for the primitive-name symbols like
either-left, either-right, and the helper names. Keep the existing :no-merge and
:merge old assertions as they are.
In `@egglog/src/proofs/proof_checker.rs`:
- Around line 962-965: The Eq-only pattern in the proof checker branch allows
bare ResolvedFact::Fact(...) to bypass container side-condition validation, so
update the handling around is_container_side_condition and the ResolvedFact
match in proof_checker to either make Fact impossible there or explicitly
reject/handle it before the early return. Use the relevant proof-checking path
in the branch that destructures ResolvedFact::Eq to ensure all container facts
are checked, including any ResolvedFact::Fact case.
---
Nitpick comments:
In `@egglog-experimental/src/container_primitives.rs`:
- Around line 193-245: The `bound_merge` runtime path and
`validate_maybe_either_i64_bool_merge` validator duplicate the same `Min`/`Max`
keep_old logic for `i64` and `bool`, so refactor that predicate into shared
helper(s) and have both functions call them. Use the existing `BoundMergeKind`,
`bound_merge`, and `validate_maybe_either_i64_bool_merge` symbols to centralize
the comparison behavior and keep the runtime and validator in sync.
In `@egglog-experimental/src/maybe.rs`:
- Around line 184-264: The float-tolerance merge condition is duplicated between
the `maybe-f64-merge-with-tol` primitive closure and
`validate_maybe_f64_merge_with_tol`, so update both paths to use one shared
helper for the numeric comparison. Extract the `old_f/new_f/tolerance` merge
check into a reusable function and call it from both
`add_primitive_with_validator!` and the validator, keeping
`maybe_sorts`/`maybe_f64` flow unchanged.
In `@egglog/scripts/nightly_bench.py`:
- Around line 303-355: The per-benchmark processing loop in nightly_bench.py
should be made resilient so one failing benchmark does not abort the full
report. Wrap the body of the benchmark iteration around the calls to probe(),
measure_cell(), hyperfine(), and any JSON loading path in a try/except that
catches unexpected exceptions like OSError and json.JSONDecodeError, then record
the current benchmark in skipped with an appropriate error reason and continue.
Keep the existing row/skip bookkeeping in the loop around benchmark names, and
use the existing probe, measure_cell, and skipped/rows flow to preserve output
for all remaining benchmarks.
In `@egglog/scripts/requirements.txt`:
- Line 1: The eval-live dependency is currently floating on the default branch,
which makes nightly runs non-reproducible; update the requirement in
requirements.txt to pin eval-live to a specific commit SHA instead of an
unpinned git reference. Keep the existing git-based dependency form, but replace
the branch-tracking reference with a commit-specific one so future upstream
changes do not alter harness behavior unexpectedly.
In `@egglog/tests/files.rs`:
- Around line 430-446: The proof trial generation in files.rs can bypass the
manual proof-disable guard for curated integration files because the check for
manual_proof_disable_reason only runs under supports_proofs, while
is_curated_proof_integration() still enables proof_testing trials. Update the
trial-building logic around push_trial in the proof-testing branch so
manual_proof_disable_reason is consulted before adding any proof_testing or
desugar proof trials, regardless of whether the run came from supports_proofs or
is_curated_proof_integration(). Use the existing Run fields and the proof
integration gating in this loop to keep disabled files from ever producing proof
trials.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: defaults
Review profile: CHILL
Plan: Pro
Run ID: ed3cb262-e3d1-4ef0-8666-cd0981e4825d
⛔ Files ignored due to path filters (23)
Cargo.lockis excluded by!**/*.lockegglog-experimental/tests/fixtures/eggcc-2mm-pass1-merge-old.eggis excluded by!**/*.eggegglog-experimental/tests/proofs/unstable-fresh-proof.eggis excluded by!**/*.eggegglog-experimental/tests/snapshots/files__proof_integration_eggcc_2mm_pass1_merge_old.snapis excluded by!**/*.snapegglog-experimental/tests/snapshots/files__proof_unit_unstable_fresh_proof.snapis excluded by!**/*.snapegglog/src/proofs/snapshots/egglog__proofs__proof_tests__tests__doc_example_add_function1.snapis excluded by!**/*.snapegglog/tests/container-proofs.eggis excluded by!**/*.eggegglog/tests/proofs/container-set-collapse.eggis excluded by!**/*.eggegglog/tests/proofs/rule-head-fast-path.eggis excluded by!**/*.eggegglog/tests/snapshots/files__proof_integration__eqsolve_desugar_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proof_integration__eqsolve_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proof_integration__integer_math_desugar_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proof_integration__integer_math_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proof_integration__math_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proof_integration__resolution_desugar_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proof_integration__resolution_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proof_integration__rw_analysis_desugar_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proof_integration__rw_analysis_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proof_manual_disabled_files.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proof_unsupported_files.snapis excluded by!**/*.snapegglog/tests/snapshots/files__shared_snapshot_container_proofs.snapis excluded by!**/*.snapegglog/tests/snapshots/files__shared_snapshot_container_set_collapse.snapis excluded by!**/*.snapegglog/tests/snapshots/files__shared_snapshot_rule_head_fast_path.snapis excluded by!**/*.snap
📒 Files selected for processing (55)
.github/workflows/build.ymlAGENTS.mdREADME.mdbench.pyegglog-experimental/Cargo.tomlegglog-experimental/src/container_primitives.rsegglog-experimental/src/either.rsegglog-experimental/src/lib.rsegglog-experimental/src/main.rsegglog-experimental/src/maybe.rsegglog-experimental/src/set_cost.rsegglog-experimental/tests/eggcc_2mm_proof.rsegglog-experimental/tests/files.rsegglog/.gitignoreegglog/CHANGELOG.mdegglog/Makefileegglog/core-relations/src/containers/mod.rsegglog/core-relations/src/containers/tests.rsegglog/core-relations/src/hash_index/mod.rsegglog/core-relations/src/hash_index/tests.rsegglog/core-relations/src/lib.rsegglog/core-relations/src/table_spec.rsegglog/core-relations/src/uf/mod.rsegglog/egglog-bridge/src/tests.rsegglog/scripts/nightly_bench.pyegglog/scripts/requirements.txtegglog/src/ast/desugar.rsegglog/src/ast/mod.rsegglog/src/ast/parse.rsegglog/src/lib.rsegglog/src/prelude.rsegglog/src/proofs/mod.rsegglog/src/proofs/proof_checker.rsegglog/src/proofs/proof_container_rebuild.rsegglog/src/proofs/proof_encoding.mdegglog/src/proofs/proof_encoding.rsegglog/src/proofs/proof_encoding_helpers.rsegglog/src/proofs/proof_extraction.rsegglog/src/proofs/proof_format.rsegglog/src/proofs/proof_normal_form.rsegglog/src/proofs/proof_simplification.rsegglog/src/proofs/proof_tests.rsegglog/src/scheduler.rsegglog/src/sort/fn.rsegglog/src/sort/map.rsegglog/src/sort/mod.rsegglog/src/sort/multiset.rsegglog/src/sort/pair.rsegglog/src/sort/set.rsegglog/src/sort/vec.rsegglog/src/termdag.rsegglog/src/typechecking.rsegglog/tests/container_rebuild.rsegglog/tests/files.rstest_bench.py
💤 Files with no reviewable changes (1)
- .github/workflows/build.yml
Owner
Author
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Pulls in egglog main, egraphs-good/egglog-experimental#56, and egraphs-good/egglog#914 (to fix some panics), so that we can have a working eggcc benchmark.
It also cleans up the testing, so that we can run proof focused testing easily:
The unit tests are in the
proofs/subdirectory and the integration tests are a list of hard coded files that are run in proof testing mode, like eggcc. That way their proofs are saved as snapshots.I tried to add hardboiled, but failed because it uses unstable function. Also luminal failed to run in proof mode.
Summary by CodeRabbit
map-ofcanonical map representation and deterministic term ordering.check-based benchmark files.